natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
equality (definitional, propositional, computational, judgemental, extensional, intensional, decidable)
identity type, equivalence of types, definitional isomorphism
isomorphism, weak equivalence, homotopy equivalence, weak homotopy equivalence, equivalence in an (∞,1)-category
Examples.
By intensional type theory one means (but see Rem. ) the flavor of type theory in which identity types are not forced to be mere propositions (that is: not necessarily (-1)-truncated).
The original definition of identity types in Martin-Löf dependent type theory [Martin-Löf (1975, §1.7 and p. 94)] is by default intensional: It takes an additional axiom or rule — the identity reflection rule, cf. Streicher (1993, p. 4, 13 ); Hofmann (1995, p. 16) — to turn intensional into extensional type theory (in which identity types are then truncated to mere propositions).
In particular, homotopy type theory is intensional: the categorical semantics of its identity types are path space objects.
(terminology)
Beware that some authors take the words “intensional type theory” to refer to type theories which fail to satisfy function extensionality. This is in general a requirement orthogonal to the (-1)-truncation of identity types.
Generally, the origin of the names “extensional” and “intensional” is somewhat confusing. Even where the term refers to the behaviour of equality, it in fact refers not to the typal equality expressed by identity types, but to judgmental equality:
The idea is that the identity type is always an “extensional” notion of equality (although it can be more or less extensional, depending on whether further extensionality principles like function extensionality and univalence hold). Thus, if the judgmental equality coincides with the identity type, then the former is also extensional, whence the type theory is called “extensional” — while if the two equalities do not coincide, then the judgmental equality has room to be more intensional than the identity type, making the type theory “intensional” (but see also Hofmann (1995, ftn. 3), p. 17).
(On this historical reading, “extensional type theory” should refer only to judgmentally extensional type theory with the reflection rule, which is much stronger than merely requiring all types to be h-sets.)
Only the intensional but not the extensional Martin-Löf type theory has decidable type checking. (Martin-Löf 75, Hofmann 95).
Per Martin-Löf, An intuitionistic theory of types: predicative part, in: H. E. Rose, J. C. Shepherdson (eds.), Logic Colloquium ‘73, Proceedings of the Logic Colloquium, Studies in Logic and the Foundations of Mathematics 80 Pages 73-118, Elsevier 1975 (doi:10.1016/S0049-237X(08)71945-1, CiteSeer)
Thomas Streicher, Investigations into Intensional Type Theory, Habilitation Thesis, Darmstadt (1993) [pdf, pdf]
Martin Hofmann, Extensional concepts in intensional type theory, Ph.D. thesis, University of
Edinburgh, (1995) (ECS-LFCS-95-327, pdf)
Last revised on January 19, 2023 at 03:03:52. See the history of this page for a list of all contributions to it.